perm filename BLOCKS[W83,JMC] blob
sn#705091 filedate 1983-03-31 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00007 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 blocks[w83,jmc] Blocks axioms using circumscription
C00004 00003 Files with blocks axioms
C00005 00004 THE BLOCKS WORLD IN SITUATION CALCULUS
C00007 00005 Introduction
C00008 00006 In this note we give several axiomatizations of the effects
C00021 00007 matters to treat
C00023 ENDMK
C⊗;
blocks[w83,jmc] Blocks axioms using circumscription
;;; only one letter sequence for each sort of variable - followed by digits
(axiom |∀x l s.at(x,l,result(move(x,l),s))|)
(axiom |∀x l s.at(x,l,move(x,l,s))|)
;;; It would be nice to have such simple axioms, but there are premisses
;;; for the successful conclusion of the action of moving something.
;;; What about
(axiom |∀x l s.normally at(x,l,move(x,l,s))|)
where normally could be taken as a modal operator, but it would be
better to interpret at(x,p,move(x,p,s)) as an object to which
;;; normally can be applied as a predicate.
Alternatively
(axiom |∀x l s.normally(at(x,l),move(x,l,s))|)
and
(axiom |∀p s.normally(p,s) ∧ ¬prevented(p,s) ⊃ holds(p,s)|)
frame:
(axiom |∀p s.primary p ∧ ¬changes(e,p,s) ∧ holds(p,s) ⊃ holds(p,result(e,s))|)
(
1. If we want to use normally, we really must handle quantifiers
under it.
2. What axioms are required in order to permit inferring "Robby built
a traffic light", "Robby built the traffic light on block A or whose
base is block A"?
Files with blocks axioms
blocks.ax[w78,jmc] FOL, includes colors and creation
BLOCK2.AX[W78,JMC] 24-Jan-78 Axioms for 4 blocks, start on towers
MOVOLD.AX[W78,JMC] 01-Feb-78 Axioms for moving, includes towers
MOVE.AX[W78,JMC] 09-Feb-78 More move axioms, reachable becomes implausible
BLOCKS.AX[W76,JMC] 13-Feb-76 Old blocks axioms - superseded
BLOCKS.NOT[W78,JMC] 27-Jan-78 Notes on blocks axiomatizations
BLOCKS.226[F75,JMC] 07-Jan-76 PROBLEMS WITH THE BLOCKS WORLD
collaboration of robots in construction;
doesn't say anything about blocks
blocks[e80,jmc]
plan.226[e78,jmc]/2p Blocks is key initial topic
THE BLOCKS WORLD IN SITUATION CALCULUS
by John McCarthy
Stanford University
Abstract: The blocks world provides a simple domain for testing
ways of representing facts about the effects of actions. This
paper presents several ways of axiomatizing facts about moving
and painting blocks using the "situation calculus" introduced
in (McCarthy and Hayes 1969). The frame and qualification
problems are illustrated and several ways of dealing with them
are proposed. Some of them use circumscription, a method of
non-monotonic reasoning proposed in (McCarthy 1980). We also
discuss some new problems that arise when we try to separate
the notions of design of an object meeting specifications from
making a plan for constructing it. The axiomatizations are in
first order languages except that circumscription is most
conveniently formalized using second order logic in a limited
way.
Introduction
(McCarthy 1960) proposed a program whose intelligent behavior
is based on representing what it knows as sentences in a logical
language and deciding what to do by deducing that a certain action
should be done. (McCarthy and Hayes 1969) introduces a formalism
that has been called "situation calculus".
In this note we give several axiomatizations of the effects
of moving and painting blocks. One object is to illustrate the
frame problem and various ways of dealing with it. These include
methods based on assignment and methods based on circumscription.
We begin with an axiomatization in which the
frame conditions are expressed directly. In these axioms
the ontology includes blocks, denoted by x,
colors, denoted by c and situations
denoted by s. When we need more than one variable, we use numerical
postscripts, and when we want to denote constants, we'll use initial capital
letters (as in proper names).
∀x x1 s.clear(x,s) ∧ clear(x1,s) ⊃
on(x,x1,move(x,x1,s))
∧ (∀x2 x3.x2 ≠ x ⊃ (on(x2,x3,move(x,x1,s)) ≡ on(x2,x3,s)))
∧ (∀x2.color(x2,move(x,x1,s)) = color(x2,s))
We get a slight shortening of this axiom if we use λ-notation to avoid
repeating the new situation move(x,x1,s).
∀x x1 s.clear(x,s) ∧ clear(x1,s) ⊃
(λs1.on(x,x1,s1) ∧ (∀x2 x3.x2 ≠ x ⊃ (on(x2,x3,s1) ≡ on(x2,x3,s)))
∧ (∀x2.color(x2,s1) = color(x2,s)))
(move(x,x1,s))
We will use λ-expressions for this purpose in subsequent axioms.
The above axiom expresses the following facts: (1) Moving the block x
to the block x1 gives rise to a new situation move(x,x1,s) which
the lambda notation allows us to call s1. (2) The axiom predicts
what happens only if both x and x1 are clear in s. (3) In this
case, x is on x1 in the new situation s1. (4) If x2 ≠ x, then
x2 is on exactly the same blocks in s1 as in s. (5) The colors
of blocks are the same in s1 as in s.
∀x s.clear(x,s) ≡ ∀x1.¬on(x1,x,s)
This defines the notion of a block being clear.
∀x c s.(λs1.color(x,s1) = c ∧ (∀x1 x2.on(x1,x2,s1) ≡ on(x1,x2,s))
∧ (∀x1.x1≠x ⊃ color(x,s1) = color(x,s)))
(paint(x,c,s))
Painting a block changes its color but doesn't change the color
of any other block and doesn't move any blocks. Painting is always
possible.
∀x x1 x2 s.on(x,x1,s) ∧ on(x,x2,s) ⊃ x1 = x2
This static rule, stating that a block cannot be on more than one other, is
used to show that a block that has been moved is not on what it was
on previously.
The next way of axiomatizing the blocks world is similar, but it uses
the formula x1 = location(x,s) instead of on(x,x1,s). This will make
comparison simpler with the later groups of axioms in which it is more
natural to use location than on. Using a function symbol makes it
implicit that every block has a location, which was not implied by the
previous set of axioms. Allowing the value of location(x,s) to be a
block x rather than something like top(x), simplifies the ontology at
the cost of generality.
∀x x1 s.clear(x,s) ∧ clear(x1,s) ⊃
(λs1.location(x,s1) = x1 ∧ (∀x2.x2 ≠ x ⊃ location(x,s1) = location(x,s))
∧ ∀x2.color(x2,s1) = color(x2,s)))
(result(move(x,x1),s))
∀x s.clear(x,s) ≡ ∀x1.location(x1,s) ≠ x
∀x c s.(λs1.color(x,s1) = c ∧ (∀x2.location(x2,s1) = location(x2,s))
∧ (∀x2.x2 ≠ x ⊃ color(x2,s1) = color(x2,s)))
(result(paint(x,c),s))
In these axioms we also reify the actions move(x,x1) and paint(x,c). This
allows us to quantify over actions in subsequent formulas. We thus introduce
events (including so far only actions) into the ontology.
We regard move(x,x1,s) and result(move(x,x1),s) as synonyms and
are free to use the former notation when reifying events is not required.
Both groups of axioms suffer from the frame problem. Namely,
it is necessary to tell what each action doesn't change as well as what
it does change. If we have n actions, each affecting some quantity,
the axiom describing the effect of each action would have to mention
all the quantities not affected.
When we describe actions in English we aren't afflicted with this
problem, so we look for formalisms that avoid it.
The axioms also suffer from the qualification problem.
We asserted that the blocks must be clear for the move to occur.
But what if a block is too heavy or glued to the table. It is
desirable to describe these possibilities by separate axioms rather
than having to include each such qualification in the rule giving
the effect of moving.
Axioms using assignment
Using assignment functions as in programming
eases the frame problem. The mathematical properties of assignment were
first formalized in (McCarthy 1963), I think. The functions assign
and val are there called a and c, and situations here correspond
to states in that paper, and the first two axioms refer to assignment
in general.
∀y z s.val(y,assign(y,z,s)) = val(z,s)
∀y z y1 s.y ≠ y1 ⊃ val(y1,assign(y,z,s)) = val(y1,s)
In this formulation frame axioms are required but they can be
given once and for all. Namely, we have
∀x v s.val(x,assign(x,v,s)) = v,
and
∀x x1 v s.x1 ≠ x ⊃ val(x1,assign(x,v,s)) = val(x1,s).
If we want to consider the equality of situations, we are
are attempted to add the following two arguments by analogy with
those governing memory states (also called environments).
∀x v1 v2 s.assign(x,v2,assign(x,v1,s)) = assign(x,v2,s)
and
∀x1 x2 v1 v2 s.x1≠x2 ⊃ assign(x1,v1,assign(x2,v2,s)) = assign(x2,v2,assign(x1,v1,s)).
Now that we have these general axioms about assignment, the specific
axioms concerning blocks are written concisely.
∀x x1 s.clear(x,s) ∧ clear(x1,s) ⊃
move(x,x1,s) = assign(location(x),x1,s)
∀x c s. paint(x,c,s) = assign(color(x),c,s)
∀x s.clear(x,s) ≡ ∀x1.val(location(x1),s) ≠ x
In this formulation location(x) and color(x) are entities that
behave like variables in that they have values in situations. They are
related to our previous notions by val(location(x),s) = location(x,s)
and val(color x, s) = color(x,s).
The decision to use particular variables in writing the axioms
amounts to imposing on the subject domain a frame or co-ordinate
system. It is like a decision in thermodynamics to choose pressure
and volume as the independent state variables and to regard others
as functions of them. In the blocks world, it isn't obvious what other
choices might be made, but there are alternatives. For example, we might
define val(location x, s) in terms of the point in the plane above
which the block is located rather than in terms of the object that the
block rests on. There wouldn't be much difference in ontology or the
axioms, although our present choice would be more convenient if we sometimes
allow blocks that aren't clear to be moved and assume that they then
carry whatever is on top of them.
Axioms using circumscription
By using circumscription, we can solve the frame problem and also
the qualification problem.
∀x x1 s.¬prevented(move(x,x1),s) ⊃ value(location x,result(move(x,x1),s)) = x1
We no longer need to say what doesn't change when a block is moved.
Circumscription will get this for us.
∀x x1 x2 s.location(x2,s) = x ∨ location(x2,s) = x1 ⊃ prevented(move(x,x1),s)
This says that blocks that aren't clear are prevented from being moved.
Actually the axiom doesn't really say that they won't move, it merely
inhibits using the previous axiom to predict the consequences of moving.
If we replaced the ⊃ sign in the axiom by ≡, we would have something
equivalent to the first set of axioms - the only possible inhibition to
moving would be non-clearness.
∀v.¬secondary(v) ∧ ¬changed(v,e,s) ⊃ value(v,result(e,s)) = value(v,s)
∀x c s. ¬prevented(paint(x,c),s) ⊃ color(x,result(paint(x,c),s)) = c
The predicates prevented and changed are to be circumscribed with
prevented having higher priority.
It is now convenient to add more conditions that might prevent
moving or painting a block. For example we could have
∀x x1 s.tooheavy x ⊃ prevented(move(x,x1),s)
Axioms using causality
∀x x1.causes(move(x,x1), location x equal x1)
∀x c.causes(paint(x,c), color x equal c)
∀x x1 x2.prevents(location x2 equal x, move(x,x1))
∀x x1 x2.prevents(location x2 equal x1, move(x,x1))
∀e p s.causes(e,p) ∧ (∀p1.prevents(p1,e) ⊃ ¬holds(p1,s)) ⊃ holds(p, result(e,s))
∀p e s.primary p ∧ ¬changes(e, p, s) ∧ holds(p,s) ⊃ holds(p, result(e,s))
matters to treat
1. do a specific situation
2. different named blocks are different
3. only the named blocks are present.
Consider applying the above general blocks axioms to a specific
situation S0 in which block X1 is on block X2 which is on the
table and there is also block X3 on the table and these are all
the blocks there are. In Formalism 1, we can describe this by
on(X1,X2,S0) ∧ on(X2,Table,S0) ∧ on(X3,Table,S0),
but we also need to assert that there are no other blocks on these
and that X1, X2, and X3 are all distinct. Formally we have
X1 ≠ X2 ∧ X1 ≠ X3 ∧ X2 ≠ X3
and
clear(X1,S0) ∧ clear(X3,S0).
and even
∀x.on(x,X2,S0) ⊃ x = X1.
We can then deduce
(λs.on(X1,X2,s) ∧ on(X2,X3,s) ∧ on(X3,Table,s))
(move(X1,X2,move(X2,X3,move(X2,Table,S0)))).
To conclude that a traffic light is present in a situation.
In order to refer to the traffic light, we need either a naming
facility or definite descriptions.